\newcommand{\rel}{\ensuremath{\,\mathcal{R}\,}}
\newcommand{\scontb}{\ensuremath{\sim_{\mathtt{CB}}}}
\newcommand{\sbarbc}{\ensuremath{\cong}}


\begin{definition}[Barbed Congruence]
A symmetric binary relation on processes $\rel$ is a strong barbed bisimulation iff $P \rel Q$ implies:
\begin{itemize}
\item for all $P \downarrow_{a}$, we have $Q \downarrow_{a}$;
\item for all $P \arro{} P'$, there exists $Q'$ such that $Q \arro{} Q'$ and $P' \rel Q'$.
\end{itemize}
Two processes $P, Q$ are strong barbed congruent, written $P \sbarbc Q$, if for all context $C$ there exists 
a strong barbed bisimulation $\rel$ such that $C[P] \rel C[Q]$.
\end{definition}

%Below we use "$\circ$" to stand for pseudo-application.
%\begin{definition}[Context Bisimulation]
%A symmetric binary relation on processes $\rel$ is a strong context bisimulation iff $P \rel Q$ implies:
%\begin{itemize}
%\item whenever $P \arro{~a~} P'$, there exists $Q'$ such that $Q \arro{~a~} Q'$ and $P' \rel Q'$;
%\item whenever $P \arro{~k~} F$, there exists $G$ such that $Q \arro{~k~} G$ and $C \circ F \rel C \circ G$, for all closed concretions $C$;
%\item whenever $P \arro{~\outC{k}~} C$, there exists $D$ such that $Q \arro{~\outC{k}~} D$ and $F \circ C \rel F \circ D$, for all closed abstractions $F$.
%\end{itemize}
%Strong context bisimularity, noted \scontb, is defined as the largest context bisimulation.
%\end{definition}


%%%%%%%%%%%%%%%%%%%%%%%

Below, $\mathsf{E}$ is an evaluation context (to be defined).

\begin{definition}[Context Bisimulation]
A symmetric binary relation on processes $\rel$ is a strong context bisimulation iff $P \rel Q$ implies:
\begin{itemize}
\item whenever $P \arro{~\tau~} P'$, there exists $Q'$ such that $Q \arro{~\tau~} Q'$ and $P' \rel Q'$;

\item whenever $P \arro{~\alpha~} P'$, there exists $Q'$ such that $Q \arro{~\alpha~} Q'$ and $P' \rel Q'$;

\item whenever $P = \mathsf{E}[a[R]]$ and $P \arro{\update{a}{U}} \mathsf{E}[U\langle R\rangle]$, 
then \\ $Q = \mathsf{E'}[a[S]]$ and  
 $Q \arro{\update{a}{U'}} \mathsf{E'}[U'\langle S\rangle]$ and $\mathsf{E}[U\langle R\rangle] \, \rel \, \mathsf{E'}[U'\langle S\rangle]$, 
 for some $U'$.


\item whenever $P \arro{~\outC{\update{a}{U}}} P'$, 
there exists $Q'$ such that \\
$Q  \arro{\outC{\update{a}{U'}}} Q'$ 
and $P' \parallel \mathsf{E}[U\langle R\rangle]  \, \rel \,  Q' \parallel \mathsf{E}[U'\langle R\rangle]  $, for all $\mathsf{E}, R$.
\end{itemize}
Strong context bisimularity, noted \scontb, is defined as the largest context bisimulation.
\end{definition}

